0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 3 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 1250 ms)
↳10 BOUNDS(1, n^1)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
id_inc(x) → x
id_inc(x) → s(x)
quot(x, y) → div(x, y, 0)
div(x, y, z) → if(ge(y, s(0)), ge(x, y), x, y, z)
if(false, b, x, y, z) → div_by_zero
if(true, false, x, y, z) → z
if(true, true, x, y, z) → div(minus(x, y), y, id_inc(z))
ge(x, 0) → true [1]
ge(0, s(y)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
id_inc(x) → x [1]
id_inc(x) → s(x) [1]
quot(x, y) → div(x, y, 0) [1]
div(x, y, z) → if(ge(y, s(0)), ge(x, y), x, y, z) [1]
if(false, b, x, y, z) → div_by_zero [1]
if(true, false, x, y, z) → z [1]
if(true, true, x, y, z) → div(minus(x, y), y, id_inc(z)) [1]
ge(x, 0) → true [1]
ge(0, s(y)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
id_inc(x) → x [1]
id_inc(x) → s(x) [1]
quot(x, y) → div(x, y, 0) [1]
div(x, y, z) → if(ge(y, s(0)), ge(x, y), x, y, z) [1]
if(false, b, x, y, z) → div_by_zero [1]
if(true, false, x, y, z) → z [1]
if(true, true, x, y, z) → div(minus(x, y), y, id_inc(z)) [1]
| ge :: 0:s:div_by_zero → 0:s:div_by_zero → true:false 0 :: 0:s:div_by_zero true :: true:false s :: 0:s:div_by_zero → 0:s:div_by_zero false :: true:false minus :: 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero id_inc :: 0:s:div_by_zero → 0:s:div_by_zero quot :: 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero div :: 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero if :: true:false → true:false → 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero → 0:s:div_by_zero div_by_zero :: 0:s:div_by_zero |
ge(v0, v1) → null_ge [0]
minus(v0, v1) → null_minus [0]
if(v0, v1, v2, v3, v4) → null_if [0]
null_ge, null_minus, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
div_by_zero => 1
null_ge => 0
null_minus => 0
null_if => 0
div(z', z'', z1) -{ 1 }→ if(ge(y, 1 + 0), ge(x, y), x, y, z) :|: z1 = z, z >= 0, z' = x, z'' = y, x >= 0, y >= 0
ge(z', z'') -{ 1 }→ ge(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
ge(z', z'') -{ 1 }→ 2 :|: z'' = 0, z' = x, x >= 0
ge(z', z'') -{ 1 }→ 1 :|: y >= 0, z'' = 1 + y, z' = 0
ge(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
id_inc(z') -{ 1 }→ x :|: z' = x, x >= 0
id_inc(z') -{ 1 }→ 1 + x :|: z' = x, x >= 0
if(z', z'', z1, z2, z3) -{ 1 }→ z :|: z2 = y, z >= 0, z' = 2, z3 = z, x >= 0, y >= 0, z'' = 1, z1 = x
if(z', z'', z1, z2, z3) -{ 1 }→ div(minus(x, y), y, id_inc(z)) :|: z2 = y, z >= 0, z' = 2, z3 = z, x >= 0, y >= 0, z'' = 2, z1 = x
if(z', z'', z1, z2, z3) -{ 1 }→ 1 :|: b >= 0, z2 = y, z >= 0, z'' = b, z3 = z, x >= 0, y >= 0, z' = 1, z1 = x
if(z', z'', z1, z2, z3) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
minus(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ minus(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
minus(z', z'') -{ 1 }→ 0 :|: z'' = y, y >= 0, z' = 0
minus(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
quot(z', z'') -{ 1 }→ div(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
| eq(start(V, V1, V14, V18, V19),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V18, V19),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V18, V19),0,[fun(V, Out)],[V >= 0]). eq(start(V, V1, V14, V18, V19),0,[quot(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V14, V18, V19),0,[div(V, V1, V14, Out)],[V >= 0,V1 >= 0,V14 >= 0]). eq(start(V, V1, V14, V18, V19),0,[if(V, V1, V14, V18, V19, Out)],[V >= 0,V1 >= 0,V14 >= 0,V18 >= 0,V19 >= 0]). eq(ge(V, V1, Out),1,[],[Out = 2,V1 = 0,V = V2,V2 >= 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V3 >= 0,V1 = 1 + V3,V = 0]). eq(ge(V, V1, Out),1,[ge(V4, V5, Ret)],[Out = Ret,V = 1 + V4,V4 >= 0,V5 >= 0,V1 = 1 + V5]). eq(minus(V, V1, Out),1,[],[Out = V6,V1 = 0,V = V6,V6 >= 0]). eq(minus(V, V1, Out),1,[],[Out = 0,V1 = V7,V7 >= 0,V = 0]). eq(minus(V, V1, Out),1,[minus(V8, V9, Ret1)],[Out = Ret1,V = 1 + V8,V8 >= 0,V9 >= 0,V1 = 1 + V9]). eq(fun(V, Out),1,[],[Out = V10,V = V10,V10 >= 0]). eq(fun(V, Out),1,[],[Out = 1 + V11,V = V11,V11 >= 0]). eq(quot(V, V1, Out),1,[div(V12, V13, 0, Ret2)],[Out = Ret2,V = V12,V1 = V13,V12 >= 0,V13 >= 0]). eq(div(V, V1, V14, Out),1,[ge(V15, 1 + 0, Ret0),ge(V16, V15, Ret11),if(Ret0, Ret11, V16, V15, V17, Ret3)],[Out = Ret3,V14 = V17,V17 >= 0,V = V16,V1 = V15,V16 >= 0,V15 >= 0]). eq(if(V, V1, V14, V18, V19, Out),1,[],[Out = 1,V20 >= 0,V18 = V21,V22 >= 0,V1 = V20,V19 = V22,V23 >= 0,V21 >= 0,V = 1,V14 = V23]). eq(if(V, V1, V14, V18, V19, Out),1,[],[Out = V24,V18 = V25,V24 >= 0,V = 2,V19 = V24,V26 >= 0,V25 >= 0,V1 = 1,V14 = V26]). eq(if(V, V1, V14, V18, V19, Out),1,[minus(V27, V28, Ret01),fun(V29, Ret21),div(Ret01, V28, Ret21, Ret4)],[Out = Ret4,V18 = V28,V29 >= 0,V = 2,V19 = V29,V27 >= 0,V28 >= 0,V1 = 2,V14 = V27]). eq(ge(V, V1, Out),0,[],[Out = 0,V30 >= 0,V31 >= 0,V1 = V31,V = V30]). eq(minus(V, V1, Out),0,[],[Out = 0,V32 >= 0,V33 >= 0,V1 = V33,V = V32]). eq(if(V, V1, V14, V18, V19, Out),0,[],[Out = 0,V18 = V34,V35 >= 0,V36 >= 0,V14 = V37,V38 >= 0,V1 = V38,V19 = V36,V37 >= 0,V34 >= 0,V = V35]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(quot(V,V1,Out),[V,V1],[Out]). input_output_vars(div(V,V1,V14,Out),[V,V1,V14],[Out]). input_output_vars(if(V,V1,V14,V18,V19,Out),[V,V1,V14,V18,V19],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. non_recursive : [fun/2]
2. recursive : [minus/3]
3. recursive : [ (div)/4,if/6]
4. non_recursive : [quot/3]
5. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into fun/2
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into (div)/4
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 24 is refined into CE [25]
* CE 21 is refined into CE [26]
* CE 22 is refined into CE [27]
* CE 23 is refined into CE [28]
### Cost equations --> "Loop" of ge/3
* CEs [28] --> Loop 17
* CEs [25] --> Loop 18
* CEs [26] --> Loop 19
* CEs [27] --> Loop 20
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [17]: [V,V1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [17]:
- RF of loop [17:1]:
V
V1
### Specialization of cost equations fun/2
* CE 15 is refined into CE [29]
* CE 16 is refined into CE [30]
### Cost equations --> "Loop" of fun/2
* CEs [29] --> Loop 21
* CEs [30] --> Loop 22
### Ranking functions of CR fun(V,Out)
#### Partial ranking functions of CR fun(V,Out)
### Specialization of cost equations minus/3
* CE 11 is refined into CE [31]
* CE 12 is refined into CE [32]
* CE 14 is refined into CE [33]
* CE 13 is refined into CE [34]
### Cost equations --> "Loop" of minus/3
* CEs [34] --> Loop 23
* CEs [31] --> Loop 24
* CEs [32,33] --> Loop 25
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [23]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [23]:
- RF of loop [23:1]:
V
V1
### Specialization of cost equations (div)/4
* CE 19 is refined into CE [35,36]
* CE 20 is refined into CE [37,38]
* CE 17 is refined into CE [39,40,41,42,43,44,45,46,47,48,49]
* CE 18 is refined into CE [50,51,52,53]
### Cost equations --> "Loop" of (div)/4
* CEs [53] --> Loop 26
* CEs [52] --> Loop 27
* CEs [51] --> Loop 28
* CEs [50] --> Loop 29
* CEs [36] --> Loop 30
* CEs [37,38] --> Loop 31
* CEs [39,40,42] --> Loop 32
* CEs [35] --> Loop 33
* CEs [41,43,44,45,46,47,48,49] --> Loop 34
### Ranking functions of CR div(V,V1,V14,Out)
* RF of phase [26,27]: [V,V-V1+1]
#### Partial ranking functions of CR div(V,V1,V14,Out)
* Partial RF of phase [26,27]:
- RF of loop [26:1,27:1]:
V
V-V1+1
### Specialization of cost equations start/5
* CE 3 is refined into CE [54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77]
* CE 4 is refined into CE [78]
* CE 2 is refined into CE [79]
* CE 5 is refined into CE [80]
* CE 6 is refined into CE [81,82,83,84,85]
* CE 7 is refined into CE [86,87,88]
* CE 8 is refined into CE [89,90]
* CE 9 is refined into CE [91,92,93,94,95,96,97,98]
* CE 10 is refined into CE [99,100,101,102,103,104,105,106]
### Cost equations --> "Loop" of start/5
* CEs [82,86,93,101] --> Loop 35
* CEs [64,71] --> Loop 36
* CEs [54,55,56,57,58,59,60,61,62,63,65,66,67,68,69,70,72,73,74,75,76,77] --> Loop 37
* CEs [78] --> Loop 38
* CEs [80] --> Loop 39
* CEs [79,81,83,84,85,87,88,89,90,91,92,94,95,96,97,98,99,100,102,103,104,105,106] --> Loop 40
### Ranking functions of CR start(V,V1,V14,V18,V19)
#### Partial ranking functions of CR start(V,V1,V14,V18,V19)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[17],20]: 1*it(17)+1
Such that:it(17) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[17],19]: 1*it(17)+1
Such that:it(17) =< V1
with precondition: [Out=2,V1>=1,V>=V1]
* Chain [[17],18]: 1*it(17)+0
Such that:it(17) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [20]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [19]: 1
with precondition: [V1=0,Out=2,V>=0]
* Chain [18]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun(V,Out):
* Chain [22]: 1
with precondition: [V+1=Out,V>=0]
* Chain [21]: 1
with precondition: [V=Out,V>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[23],25]: 1*it(23)+1
Such that:it(23) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[23],24]: 1*it(23)+1
Such that:it(23) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [25]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [24]: 1
with precondition: [V1=0,V=Out,V>=0]
#### Cost of chains of div(V,V1,V14,Out):
* Chain [[26,27],34]: 12*it(26)+8*s(3)+4*s(5)+6*s(7)+2*s(29)+3
Such that:aux(1) =< 1
aux(9) =< V-V1+1
aux(3) =< V1
aux(12) =< V
s(3) =< aux(1)
s(7) =< aux(12)
s(5) =< aux(3)
aux(6) =< aux(12)
it(26) =< aux(12)
aux(6) =< aux(9)
it(26) =< aux(9)
s(29) =< aux(6)
with precondition: [Out=0,V1>=1,V14>=0,V>=V1]
* Chain [[26,27],33]: 12*it(26)+2*s(29)+2*s(30)+2*s(33)+1*s(35)+4
Such that:s(35) =< 1
aux(9) =< V-V1+1
s(31) =< V+V14-Out
aux(13) =< V
aux(6) =< aux(13)
it(26) =< aux(13)
aux(6) =< aux(9)
it(26) =< aux(9)
s(29) =< aux(6)
s(33) =< aux(13)
s(30) =< s(31)
with precondition: [V1>=1,V14>=0,V>=V1,Out>=V14,V+V14+1>=Out+V1]
* Chain [[26,27],30]: 12*it(26)+2*s(29)+2*s(30)+3*s(33)+1*s(36)+4
Such that:s(36) =< 1
aux(9) =< V-V1+1
s(31) =< V+V14-Out
aux(14) =< V
s(33) =< aux(14)
aux(6) =< aux(14)
it(26) =< aux(14)
aux(6) =< aux(9)
it(26) =< aux(9)
s(29) =< aux(6)
s(30) =< s(31)
with precondition: [V1>=2,V14>=0,V>=V1+1,Out>=V14,V+2*V14+1>=2*Out+V1]
* Chain [[26,27],29,34]: 12*it(26)+9*s(3)+6*s(5)+2*s(29)+2*s(30)+2*s(33)+9
Such that:aux(16) =< 1
aux(8) =< V
aux(9) =< V-V1+1
aux(17) =< V1
aux(18) =< V-V1
s(3) =< aux(16)
s(5) =< aux(17)
aux(6) =< aux(8)
it(26) =< aux(8)
s(34) =< aux(8)
aux(6) =< aux(9)
it(26) =< aux(9)
aux(6) =< aux(18)
it(26) =< aux(18)
s(34) =< aux(18)
s(29) =< aux(6)
s(33) =< s(34)
s(30) =< aux(18)
with precondition: [Out=0,V1>=1,V14>=0,V>=2*V1]
* Chain [[26,27],29,33]: 12*it(26)+2*s(29)+2*s(30)+2*s(33)+2*s(35)+2*s(39)+10
Such that:aux(19) =< 1
aux(8) =< V
aux(9) =< V-V1+1
s(31) =< V-V1+V14-Out+1
aux(15) =< V1
aux(20) =< V-V1
s(35) =< aux(19)
s(39) =< aux(15)
aux(6) =< aux(8)
it(26) =< aux(8)
s(34) =< aux(8)
aux(6) =< aux(9)
it(26) =< aux(9)
aux(6) =< aux(20)
it(26) =< aux(20)
s(34) =< aux(20)
s(29) =< aux(6)
s(33) =< s(34)
s(30) =< s(31)
with precondition: [V1>=1,V14>=0,V>=2*V1,Out>=V14+1,V+V14+2>=2*V1+Out]
* Chain [[26,27],28,34]: 12*it(26)+9*s(3)+6*s(5)+2*s(29)+2*s(30)+2*s(33)+9
Such that:aux(22) =< 1
aux(8) =< V
aux(9) =< V-V1+1
aux(23) =< V1
aux(24) =< V-V1
s(3) =< aux(22)
s(5) =< aux(23)
aux(6) =< aux(8)
it(26) =< aux(8)
s(34) =< aux(8)
aux(6) =< aux(9)
it(26) =< aux(9)
aux(6) =< aux(24)
it(26) =< aux(24)
s(34) =< aux(24)
s(29) =< aux(6)
s(33) =< s(34)
s(30) =< aux(24)
with precondition: [Out=0,V1>=1,V14>=0,V>=2*V1]
* Chain [[26,27],28,33]: 12*it(26)+2*s(29)+2*s(30)+2*s(33)+2*s(35)+2*s(42)+10
Such that:aux(25) =< 1
aux(8) =< V
aux(9) =< V-V1+1
s(31) =< V-V1+V14-Out
aux(21) =< V1
aux(26) =< V-V1
s(35) =< aux(25)
s(42) =< aux(21)
aux(6) =< aux(8)
it(26) =< aux(8)
s(34) =< aux(8)
aux(6) =< aux(9)
it(26) =< aux(9)
aux(6) =< aux(26)
it(26) =< aux(26)
s(34) =< aux(26)
s(29) =< aux(6)
s(33) =< s(34)
s(30) =< s(31)
with precondition: [V1>=1,V14>=0,V>=2*V1,Out>=V14,V+V14+1>=2*V1+Out]
* Chain [34]: 8*s(3)+4*s(5)+2*s(7)+3
Such that:aux(1) =< 1
aux(2) =< V
aux(3) =< V1
s(3) =< aux(1)
s(7) =< aux(2)
s(5) =< aux(3)
with precondition: [Out=0,V>=0,V1>=0,V14>=0]
* Chain [33]: 1*s(35)+4
Such that:s(35) =< 1
with precondition: [V=0,V14=Out,V1>=1,V14>=0]
* Chain [32]: 4
with precondition: [V1=0,Out=0,V>=0,V14>=0]
* Chain [31]: 4
with precondition: [V1=0,Out=1,V>=0,V14>=0]
* Chain [30]: 1*s(36)+1*s(37)+4
Such that:s(36) =< 1
s(37) =< V
with precondition: [V14=Out,V>=1,V14>=0,V1>=V+1]
* Chain [29,34]: 9*s(3)+6*s(5)+9
Such that:aux(16) =< 1
aux(17) =< V1
s(3) =< aux(16)
s(5) =< aux(17)
with precondition: [Out=0,V1>=1,V14>=0,V>=V1]
* Chain [29,33]: 2*s(35)+2*s(39)+10
Such that:aux(15) =< V1
aux(19) =< 1
s(35) =< aux(19)
s(39) =< aux(15)
with precondition: [Out=V14+1,V1>=1,Out>=1,V>=V1]
* Chain [28,34]: 9*s(3)+6*s(5)+9
Such that:aux(22) =< 1
aux(23) =< V1
s(3) =< aux(22)
s(5) =< aux(23)
with precondition: [Out=0,V1>=1,V14>=0,V>=V1]
* Chain [28,33]: 2*s(35)+2*s(42)+10
Such that:aux(21) =< V1
aux(25) =< 1
s(35) =< aux(25)
s(42) =< aux(21)
with precondition: [V14=Out,V1>=1,V14>=0,V>=V1]
#### Cost of chains of start(V,V1,V14,V18,V19):
* Chain [40]: 84*s(119)+37*s(120)+128*s(124)+96*s(134)+16*s(136)+16*s(137)+16*s(138)+72*s(140)+12*s(141)+11
Such that:aux(42) =< 1
aux(43) =< V
aux(44) =< V-V1
aux(45) =< V-V1+1
aux(46) =< V1
s(124) =< aux(42)
s(120) =< aux(43)
s(119) =< aux(46)
s(133) =< aux(43)
s(134) =< aux(43)
s(135) =< aux(43)
s(133) =< aux(45)
s(134) =< aux(45)
s(133) =< aux(44)
s(134) =< aux(44)
s(135) =< aux(44)
s(136) =< s(133)
s(137) =< s(135)
s(138) =< aux(44)
s(139) =< aux(43)
s(140) =< aux(43)
s(139) =< aux(45)
s(140) =< aux(45)
s(141) =< s(139)
with precondition: [V>=0]
* Chain [39]: 1
with precondition: [V=1,V1>=0,V14>=0,V18>=0,V19>=0]
* Chain [38]: 1
with precondition: [V=2,V1=1,V14>=0,V18>=0,V19>=0]
* Chain [37]: 336*s(257)+32*s(259)+72*s(261)+12*s(263)+160*s(286)+8*s(302)+36*s(336)+96*s(338)+16*s(340)+16*s(341)+16*s(342)+72*s(344)+12*s(345)+13
Such that:aux(67) =< 1
aux(68) =< V14
aux(69) =< V14+1
aux(70) =< V14-2*V18
aux(71) =< V14-2*V18+1
aux(72) =< V14-V18
aux(73) =< -V18
aux(74) =< V18
s(257) =< aux(67)
s(336) =< aux(72)
s(286) =< aux(74)
s(259) =< aux(68)
s(260) =< aux(68)
s(261) =< aux(68)
s(260) =< aux(69)
s(261) =< aux(69)
s(263) =< s(260)
s(302) =< aux(73)
s(337) =< aux(72)
s(338) =< aux(72)
s(339) =< aux(72)
s(337) =< aux(71)
s(338) =< aux(71)
s(337) =< aux(70)
s(338) =< aux(70)
s(339) =< aux(70)
s(340) =< s(337)
s(341) =< s(339)
s(342) =< aux(70)
s(343) =< aux(72)
s(344) =< aux(72)
s(343) =< aux(71)
s(344) =< aux(71)
s(345) =< s(343)
with precondition: [V=2,V1=2,V14>=0,V18>=0,V19>=0]
* Chain [36]: 2*s(466)+2*s(467)+7
Such that:aux(75) =< 1
aux(76) =< V18
s(467) =< aux(75)
s(466) =< aux(76)
with precondition: [V=2,V1=2,V14=V18,V14>=1,V19>=0]
* Chain [35]: 5
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V14,V18,V19):
-------------------------------------
* Chain [40] with precondition: [V>=0]
- Upper bound: 249*V+139+nat(V1)*84+nat(V-V1)*16
- Complexity: n
* Chain [39] with precondition: [V=1,V1>=0,V14>=0,V18>=0,V19>=0]
- Upper bound: 1
- Complexity: constant
* Chain [38] with precondition: [V=2,V1=1,V14>=0,V18>=0,V19>=0]
- Upper bound: 1
- Complexity: constant
* Chain [37] with precondition: [V=2,V1=2,V14>=0,V18>=0,V19>=0]
- Upper bound: 116*V14+160*V18+349+nat(V14-V18)*248+nat(V14-2*V18)*16
- Complexity: n
* Chain [36] with precondition: [V=2,V1=2,V14=V18,V14>=1,V19>=0]
- Upper bound: 2*V18+9
- Complexity: n
* Chain [35] with precondition: [V1=0,V>=0]
- Upper bound: 5
- Complexity: constant
### Maximum cost of start(V,V1,V14,V18,V19): max([max([4,249*V+138+nat(V1)*84+nat(V-V1)*16]),nat(V14)*116+340+nat(V18)*158+nat(V14-V18)*248+nat(V14-2*V18)*16+ (nat(V18)*2+8)])+1
Asymptotic class: n
* Total analysis performed in 1020 ms.